% Several studies have investigated transformation verification with
% respect to different kinds of properties, e.g. structural correspondance between
% input and output models~\cite{LEVI,CRSP}, correctness with respect to
% domain-specific constraints~\cite{ANAS,VQVT,REFC,DEDU}.
%another ex, LTL props, depth
% We summarize studies that investigated verifying transformations with respect to
% domain-specific constraints, similar to our study.
%
% This formalization was done on two phases. First, the
% UML2Alloy tool was used to translate the metamodels and their OCL constraints to
% Alloy models. Second, the transformation was transformed to an Alloy model by
% expressing the transformation rules in first-order logic and introducing a
% \emph{mapping relation} in Alloy to keep track of the mapping between input and
% output model elements. 
%
There are several approaches that translate declarative model transformations
into some logic or logic-like language to perform automated verification.
Anastasakis \emph{et al.}~\cite{ANAS} and Baresi and Spoletini~\cite{Baresi2006}
use relational logic and the Alloy analyzer to check for inconsistencies in a
transformation.
%
Inaba \emph{et al.}~\cite{Inaba2011} verify the typing of transformations with
respect to a metamodel using second-order monadic logic and the MONA solver.
%
Troya and Vallecillo~\cite{Troya2011ATL} define an encoding of ATL in rewriting
logic, that can be used to check the possible executions of a transformation in
Maude.
%
Cabot \emph{et al.}~\cite{Cabot2010} translated QVT-R and triple graph grammar
transformations into OCL contracts, requiring an OCL model finder to conduct the
counterexample checking. Our translation of ATL into OCL (based
on~\cite{Buettner2012ICFEM}) closely resembles this approach.
%
In another previous work~\cite{Buettner2012MoDELS}, we have presented a mapping
of ATL directly into first-order logic, using quantifier reasoning to prove
transformation properties with SMT solvers.

Asztalos \emph{et al.}~\cite{DEDU} formulated transformations and their
properties as assertions in first-order logic. A deduction system was
implemented to deduce the properties from the rules.
%
Lucio \emph{et al.}~\cite{LEVI} verified correctness constraints for
transformations in DSLTrans language using a model checker implemented in
Prolog.
Rensink~\cite{Rensink2008} checked first-order linear temporal properties for
graph transformation systems.  Becker \emph{et
al.}~\cite{REFC} verified a metamodel refactoring implemented as a graph
rewriting system by extending the metamodel with predicate structures which were
used to specify well-formedness graph constraints. 
%
Stenzel \emph{et al.}~\cite{VQVT} implemented an algebraic formalization of a
subset of operational QVT in the KIV theorem prover. 
%  A QVT transformation and
% its properties were specified in terms of the proposed formalization and KIV was
% used to verify the specified properties.

% TRANSFORMATION CONTRACTS
There are also several approaches that use OCL constraints to specify contracts
for model transformations.  Guerra \emph{et al.}~\cite{Guerra2013}, Gogolla and
Vallecillo~\cite{GOGO}, Braga \emph{et al.}~\cite{Braga2011}, and Cariou
\emph{et al.}~\cite{Cariou2009} discussed testing transformations against contracts.
In the same vein, Narayanan \emph{et al.}~\cite{CRSP} discuss a methodology to
specify structural correspondence rules between source and target. Our constraints
presented in Sect.~\ref{subsec:FormulationOCLConsts} can be considered a
transformation contract in this sense, although we do not use the contracts to
test the actual transformation implementation but use them to verify the
transformation independent of any input.%on the logic level.

%MODEL FINDERS
Regarding the used approach to check the satisfiability of OCL-constrained
models, there are several potential alternatives to the USE Model
Validator~\cite{Kuhlmann2011} that we employed.  Gonzalez \emph{et
al.}~\cite{Gonzalez2012} implemented the EMFtoCSP model finder that encodes
metamodels and OCL constraints as constraint-logic programs (performing bounded
verification).  Queralt and Teniente~\cite{Queralt2012} implemented a symbolic
reasoning procedure for OCL constraints, based on predicate calculus.  Brucker
\emph{et al.}~\cite{Brucker2009} implemented the HOL-OCL theorem prover to
interactively prove correctness constraints. Jackson \emph{et
  al.}~\cite{Jackson2013} used the FORMULA tool to reason about metamodels, but
they did not support OCL.
%for transformation verification
% by formalizing a transformation and its manipulated metamodels as Alloy
% models. The Alloy analyzer was then used to verify the transformation in
% several ways. First, the Alloy analyzer was used to generate an instance of the
% transformation model. Failure to produce a transformation instance implied that
% the transformation had inconsistencies which could be resolved using the Alloy
% analyzer. Second, the Alloy analyzer was used to produce several transformation
% instances to investigate different mappings between the source
% and target metamodels. Finally, the Alloy analyzer was used to perform assertion
% checking. A case study showed that the approach was not scalable, applicable
% only to declarative transformations, can only analyze integer properties of the
% Alloy model and is not capable of reasoning about dynamic properties of the
% transformation. %, i.e. Alloy has no representation for a system's behaviour. 
% model-to-text QVT transformation that transforms UML class diagrams to Java Abstract Syntax Trees
% (JASTs) and eventually to Java classes.
% %analyze semantical properties of , and the type consistency and semantical
% %properties of the generated output.
% %\footnote{An example of a semantical property of a transformation's output code
% % is that calling a setter then the corresponding getter returns the setter's
% % argument.} \footnote{An example of a semantical property of a model-to-code
% % transformation is that each UML class is transformed to a Java class.}.
% To analyze properties of the transformation, an algebraic formalization of a
% subset of operational QVT was implemented in KIV. The transformation and it's
% properties of interest were specified in terms of the proposed formalization and
% KIV was used to verify the specified properties. 
%To analyze properties of the
%transformation's output, an Eclipse plug-in was used to transform output JAST
%models into a KIV-compatible format. The generated JAST models were transformed
%by KIV into an AST with defined properties that can be used to reason about the
%Java code. 
%A model transformation can also be analyzed for preservation of type
% consistency and multi-view consistency by analyzing its output models only.
%
% verified transformations with
% respect to a property of interest by formulating the transformation
% rules and the property of interest as assertions in first-order logic. Deduction
% rules were defined and used to deduce the property assertion from the rules'
% assertions. A prototype framework was implemented in the Visual Modeling and
% Transformation System (VMTS) which can generate assertions for a
% transformation's rules. The study claimed that their approach is extensible to
% different transformation frameworks and can be used to prove several
% properties. The approach was also found to be inefficient if complicated
% deduction rules were defined or if many assertions were used. 
%Studies from the industry on formal verification, if any ?
%Should we mention model checking? is it close to what we do?
% Gogolla and Vallecillo ~\cite{GOGO} also used the USE tool and contracts to
% verify transformations. However, their study used testing for verifying
% transformations, which is different from our approach. Our approach verifies a
% transformation independent of any input model while testing ivolves generating a
% test suite and executing the transformation using each model in the test suite.
% Further, their approach was not experimented with on industrial-size
% transformations. 
%
% Predicates were
% automatically added to the model if the model had a \emph{forbidden pattern}.
% If the refactored model overlapped with a forbidden pattern, a counterexample was
% generated.

The novel aspect of our study is two-fold: First, we have applied an automated
verification methodology to an industrial model transformation implemented in
the ATL transformation language. Second, we have shown the applicability of this
approach to realistic search spaces and discussed the performance of our
approach. Most of the referenced research papers evaluate their verification
approach on small examples and do not address the performance aspect.
% and discussed scalability aspects. 
% aforementioned studies is three ways. First,
% we demonstrate how a light-weight, automated verification prototype can be
% used to uncover bugs in an industrial transformation. Such prototypes
% are more useful than other informal verification tools, e.g. testing frameworks,
% in that they guarantee properties for transformations independent of any input,
% albeit on a bounded scope.
% Second, we discuss the performance of the used approach and hence we address its
% applicability to large, industrial transformation problems.
% Third, we manipulate a widely-used transformation language, ATL, and a
% simple language for formulating constraints, OCL, which makes the approach
% easy to adopt. The user doesnot need to have a mathematical
% background to use the prototype, as is the case with theorem
% provers, e.g. ~\cite{VQVT}.
%\subsection*{SNIP}
% Troya and Vallecillo provide an encoding of ATL in rewriting logic, using Maude
% to check the possible executions of a transformation~\cite{Troya2011ATL}.
%
% Guerra et al.~\cite{Guerra2013}, Gogolla and Vallecillo~\cite{GOGO}, Braga et
% al.~\cite{Braga2011}, and Cariou et al.~\cite{Cariou2009} discuss the systematic
% testing of transformations agains a contract. Unlike us, they do not
% automatically verify a transformation implementation against its contract(s).
% 
% Inaba et al. type check transformations with respect to a schema (i.e., a metamodel) by using the MONA
% solver~\cite{Inaba2011}. Only the typing of the graph can be checked in this approach. Other properties, e.g., the uniqueness of names,  cannot  be expressed
% in this approach although they can be expressed in OCL.
% 
% Lucio et al. address similar correctness properties for the DSLTrans
% transformation language, using resolution (in Prolog) to check the
% transformation~\cite{LEVI}. In similar vein, Rensink checks first-order linear
% temporal properties for graph transformation systems~\cite{Rensink2008}.
% 
% Baresi and Spoletini also use Alloy to check graph transformation systems~\cite{Baresi2006}.
%
%Cabot et al. translate QVT-R and triple graph grammar transformations into OCL
% contracts~\cite{Cabot2010}.
%
% Other (implemented) model finding approaches (instead of using the USE validator):
% In their tool EMFtoCSP, Gonzalez et al.~\cite{Gonzalez2012} encode metamodels and OCL into constraint-logic programs. 
%
%Queralt and Teniente implemented a system of automatic reasoning rules for OCL
% in the EinaGMC project~\cite{Queralt2012}.
%
%Similarly, the approach of Jackson et al.~\cite{Jackson2013} use the FORMULA
% tool to reasons about metamodels, but they do not use or support OCL.
%
% Brucker et al. provide an theorem proving environment HOL-OCL~\cite{Brucker2009}
% that could be used to interactively prove our correctness.
% 
% (not related work, but for the first reference of ATL:~\cite{Jouault2008ATL})